KokaのEffect Types

関数の型を3箇所で表す

(引数) -> <EffectTypes> 返り値

例

このシグネチャのtotalとかexnの部分がEffect Types

code:koka(js)

fun sqr : (int) -> total int

fun divide : (int,int) -> exn int

fun turing : (tape) -> div int

fun print : (string) -> console ()

fun rand : () -> ndet int

これらはいずれも推論の対象になる

docs上ではhoverすると推論された結果を見れる

https://gyazo.com/56cdcdebb2fc101a91100230945e8a89

個々のEffect Typesを組み合わせることもできる

code:koka(js)

alias pure = <div,exn>

当然、複数のEffect Typesを持つ関数も定義できる

code:koka(js)

fun looptest()

while { is-odd(srandom-int()) }

throw("odd")

table:個々の関数の返り値

while <div|e> types/()

is-odd total bool

scrandom-int ndet int

throw exn a

従って、このlooptest()の返り値は、<pure,ndet> ()と推論される

Effect Typesはbuilt-inで用意されているものも多く、また自分で定義することもできる

built-inで用意されているものの例 ref

total, <>

全域関数である

Effectが存在しないことを表す

単位元的な

exn

例外が発生する可能性がある

部分関数である

div型

divergent

関数が終了しない可能性がある

console型

consoleに書き込む可能性がある

ndet型

非決定的

pure = <exn,div> ref

純粋関数である

exnとdivの組み合わせのことをpureと呼ぶのちょっとビビるが、まあ実際そうか

The combination of exn and div is called pure as that corresponds to Haskell's notion of purity. ref

st<h> = <read<h>,write<h>,alloc<h>>

mutablityは、read/write/allocの組み合わせ

effect typesもpolymorphicなんですなmrsekut.icon

io = <exn,div,ndet,console,net,fsys,ui,st<global>> ref

全部盛りじゃんmrsekut.icon

etc.

自分でEffect Typesを定義する ref

Effect Typesの定義

code:koka(js)

effect raise // ①

ctl raise( msg : string ) : a // ②

effectとctlがキーワード

①でraiseという名前のeffect typesを定義してる

②でそのoperationとしてraise( msg : string ) : aを定義

これらは異なる名前でも良い

typeとoperationが同じ場合は以下のように省略しても書ける

code:koka(js)

effect ctl raise(msg: string): a

Polymorphic Effects

docs

例: map : (xs : list<a>, f : (a) -> e b) -> e list<b>

mapの返り値のEffect typesは、引数fのEffect typesを引き継ぐ

< .. | e>のように書いて、effectsを追加できることを示せる

pursのRow polymorphismのsyntaxと同じだmrsekut.icon

例: while : ( pred : () -> <div|e> bool, action : () -> <div|e> () ) -> <div|e> ()

気持ち的には上のmapと同じだが、

while : ( pred : () -> e bool, action : () -> e () ) -> e ()

whileは無限ループの可能性があるので、diveffectを追加する

なので、<div|e>のようにpolymorphicでありつつも、effectsを拡張した型になる

内部の書き方を変えることでeffect typeが変わる例 ref

再帰するとdivが必要になる

code:koka(js)

fun fib(n : int) : div int

if n <= 0 then 0

elif n == 1 then 1

else fib(n - 1) + fib(n - 2)

これをmutable変数を使うことで、totalに変えられる

code:koka(js)

fun fib2(n)

var x := 0

var y := 1

repeat(n)

val y0 = y

y := x+y

x := y0

#??

types/()って型はなに？

https://koka-lang.github.io/koka/doc/std_core.html#repeat_1

普通にユニット型()のことかなmrsekut.icon

types/はmodule名でしょう

^nという表記は何？

https://koka-lang.github.io/koka/doc/std_core.html#repeat

型クラス的なものはないのか

ad hoc多相がない(?)から、同じ関数を型ごとにoverloadしまくってる

例えばshowするときにどうする？